Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant

摘要

We present the proof of Diophantus' 20th problem (book VI of Diophantus'Arithmetica), which consists in wondering if there exist right triangles whosesides may be measured as integers and whose surface may be a square. Thisproblem was negatively solved by Fermat in the 17th century, who used the"wonderful" method (ipse dixit Fermat) of infinite descent. This method, whichis, historically, the first use of induction, consists in producing smaller andsmaller non-negative integer solutions assuming that one exists; this naturallyleads to a reductio ad absurdum reasoning because we are bounded by zero. Wedescribe the formalization of this proof which has been carried out in the Coqproof assistant. Moreover, as a direct and no less historical application, wealso provide the proof (by Fermat) of Fermat's last theorem for n=4, as well asthe corresponding formalization made in Coq.